%\documentclass[a4paper,10pt]{article}
\documentclass[envcountsect,envcountsame,runningheads,a4paper]{llncs} 
% \documentclass[runningheads,a4paper]{llncs}


%\usepackage[utf8]{inputenc} \usepackage{times}
\usepackage[T1]{fontenc} \usepackage{tgtermes}

\usepackage[english]{babel}
\usepackage{xspace}
\usepackage{float}
\usepackage{mathpartir}

\usepackage{amstext, amssymb, amsfonts, amsmath}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{graphicx}
\usepackage{enumerate}

\usepackage{color}
\usepackage{url}
\usepackage{hyperref}
\usepackage{proof}

\usepackage{macron}
\usepackage{typecasemacro}


\usepackage{lineno}

\newtheorem{newnotation}[theorem]{Notation}



%opening
\title{
Runtime Adaptation in Communication-Centric Systems: An Event-Based Approach\thanks{DRAFT - Revision of \today}
%An Event-Based Architecture for Runtime Adaptation in Communication-Centric Systems
}
\titlerunning{Runtime Adaptation in Communication-Centric Systems}
\author{Cinzia Di Giusto \inst{1} \and Jorge A. P\'{e}rez\inst{2}}
\institute{%Universite d'Evry 
Universit\'{e} d'Evry - Val d'Essonne, Laboratoire IBISC, Evry
\and Johann Bernoulli Institute for Mathematics and Computer Science, University of Groningen}

\widowpenalty=0
\clubpenalty=0

\begin{document}

\maketitle



\vspace{-4mm}     
\begin{abstract}
%%Modern distributed software systems are \emph{communication-centric}: 
%%built as assemblies of software artifacts, 
%%these systems rely on consistent dialogues among such artifacts. 
%%Ensuring conformance of these dialogues to prescribed protocols is thus key to correctness.
%% As  systems become more complex, correctness analyses must unavoidably 
%% account for issues not strictly tied to communication but that influence overall   behavior.
%% This paper deals with one of such issues,
%% \emph{runtime adaptation},  here understood as the dynamic update of the behavior of part of the system.
%%Concretely, we are interested in integrating mechanisms for runtime adaptation into \emph{session types} for structured communications.
%%We offer two main contributions.
%%First, by  relying on selected features from  
%%the eventful session framework by Kouzapas et al, 
%%we propose an \emph{event-based}  approach to runtime adaptation of session typed processes.
%%Our approach enables us to  define rich forms of adaptation, 
%%even for processes with active running sessions.
%%Second,
%%we propose a simple architecture for communication-centric systems with runtime adaptation. 
%%By formalizing \emph{compartmentalized} communications, 
%%our architecture offers  an alternative for organizing session-based systems and services.
%====
%Modern distributed  systems are \emph{communication-centric}: 
%built as assemblies of software artifacts, 
%these systems rely on consistent dialogues among such artifacts. 
% As systems become more complex, the analysis of communication correctness must unavoidably 
% account for issues not strictly tied to communication but that influence overall   behavior.
% This paper addresses  one of such issues,
% \emph{runtime adaptation},  here understood as the dynamic update of the behavior of part of the system.
%Concretely, we are interested in integrating mechanisms for runtime adaptation into \emph{session types} for structured communications.
%We offer two main contributions.
%First, by  relying on selected features from the eventful session framework by Kouzapas et al, 
%we propose an \emph{event-based}  approach to runtime adaptation of session typed processes.
%Our approach improves prior works by 
%enabling rich forms of adaptation, 
%even for processes with active sessions.
%Second,
%we propose a 
%model of \emph{compartmentalized} communication-centric systems with runtime adaptation. 
%This model offers  an alternative for organizing session-based systems and services and their associated adaptation 
%mechanisms.
%====
This paper addresses  
the enhancement of  \emph{session types} for structured communications with mechanisms for \emph{runtime adaptation}---understood as the dynamic update of the behavior of part of the system.
We offer two main contributions.
First, by  relying on selected features from the eventful session framework by Kouzapas et al., 
we propose an \emph{event-based}  approach to runtime adaptation of session typed processes.
Our approach improves prior works by 
enabling rich forms of adaptation, 
even for processes with active sessions.
Second,
we propose a 
model of \emph{compartmentalized} communication-centric systems with runtime adaptation. 
This model offers  an alternative for organizing session-based systems and services and their associated adaptation 
mechanisms.
\end{abstract}
%
%\section{Suggestions}
%%The abstract can be much shorter and more general. 
%
%Mention the well-known work on exceptions for binary session types, and other session disciplines with buffers/queues~\cite{DBLP:journals/jfp/GayV10}.
%
%Before giving technical details, it would be very useful to give a concrete example for configurations/networks, and their evolution.
%The example could illustrate records, memories, etc. 

%\vspace{-2mm}    


 \linenumbers

\section{Introduction}
Modern distributed %software 
systems are \emph{communication-centric}: 
built as assemblies of software artifacts, 
these systems rely on consistent dialogues among such artifacts. 
Ensuring conformance of these dialogues to prescribed protocols is key to correctness.
In \emph{session-based concurrency},  
 dialogues are structured into %basic 
 units called sessions; interaction patterns are abstracted as \emph{session types}~\cite{DBLP:conf/esop/HondaVK98}, 
against which specifications may be checked. \looseness=-1

This paper addresses the challenge of integrating mechanisms for \emph{runtime adaptation} 
into a %typed 
model of session-based concurrency.
We build upon our prior work~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}, which 
proposed the first typeful integration of  basic runtime adaptation mechanisms.
In this paper, 
we (i)~enhance such mechanisms, and also  
(ii)~clarify their status within formal models of session-based communication.
A distinctive feature of the present development is that we follow an \emph{event-based} approach, relying on constructs from~\cite{Kouzapas12,KouzapasJ13}. 
 
As communication-centric systems are typically open, and  operate on dynamic infrastructures, 
\emph{runtime adaptation} is a key feature to ensure continued system operation. %, optimize costs, 
%and enhance business agility.
As in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}, 
%in this paper 
here we understand runtime adaptation as the dynamic modification of (the behavior of) the system as a response to an exceptional  \emph{event}, not necessarily catastrophic. 
%Formal specification(s) of the system should describe the sub-systems amenable to adaptation and their exceptional events. 
%Then, on the basis of an initial specification and its projected evolution, an array of potential adaptation routines is defined at design time. 
As such, although not strictly tied to communication, runtime adaptation may influence overall behavior.
Integrating forms of runtime adaptation into session-based concurrency is a relevant issue. 
It is also a challenging one, as correctness analysis should balance the intertwined concerns of 
structured 
communications and 
runtime adaptation.
 
To realize 
this integration,
the approach that we have pursued in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}  relies on 
%To integrate this vision of runtime adaptation into a session typed process language, i we have appealed to 
the two key constructs of the \emph{adaptable processes} framework~\cite{BGPZFMOODS}.
Given a location $\locf{loc}$ (a distinguished computation site), a process $P$, and a context $Q(\mathsf{X})$ 
(a process with zero or more occurrences of process variable $\mathsf{X}$),
the framework in~\cite{BGPZFMOODS} introduces 
so-called \emph{located processes} and \emph{update processes}, written $\scomponent{\locf{loc}}{P}$ and 
$\nadapt{\locf{loc}}{Q(\mathsf{X})}$, respectively.
These two processes may synchronize on $\locf{loc}$; by doing so, one obtains process 
$Q\subst{P}{\mathsf{X}}$, i.e., the process $Q$ in which all free occurrences of $\mathsf{X}$ are replaced with $P$.
This step represents the \emph{update} of  process $P$ at $\locf{loc}$ with an \emph{adaptation routine}
embodied by $Q$. 
%Locations can be nested and are transparent: within $\scomponent{\locf{loc}}{P}$, process $P$ may evolve autonomously, with the potential of interacting with some update process for $\locf{loc}$. 

%Combining located and update processes gives an expressive alternative for specifying 
%runtime adaptation for communicating processes. %, in the sense defined above,  for .
In~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13} we have integrated 
located and update processes
%these two constructs 
into a session-typed $\pi$-calculus. 
To address the desired balance between communication correctness and runtime adaptation, 
%in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13} 
we have proposed the \emph{consistency} property, ensuring that
 %actions over located processes which are engaged in active session behavior cannot be enabled. 
 %Intuitively, this means that adaptation 
 %actions do not jeopardize already established sessions.
 established sessions are never disrupted by adaptation actions.
%Using so-called \emph{session interfaces}, 
The techniques  used to enforce consistency ensure 
also the preservation of service definitions: this way, e.g.,
 a persistent session server %, possibly useful to different clients at different time
  is never removed as a result of an update action.
 The  type system in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}
 ensures both safety (absence of communication errors at runtime) and consistency.
While intuitive, the mechanisms and guarantees introduced in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13} are limited in two ways:
\begin{enumerate}[1.]
\item Since adaptation  takes place when a located process and an update process synchronize on some location, located and update processes should be carefully embedded within communication prefixes. 
This style of specification is well-suited for programming \emph{internal adaptation requests} (i.e. requests issued by the system itself) but is inadequate to specify \emph{external adaptation requests}, i.e. requests communicated to the system by its environment.
%Also, predicting when adaptation steps should occur can be difficult.
%This suggest that our existing mechanisms could be improved by an 
This suggests the need for an %additional %What seems to be required to enhance our mechanisms is an
 interaction layer, orthogonal to sessions, which uniformly
treats internal and external adaptation requests. % in a uniform manner.

\item Consistency may  be overly protective.
For instance, 
an adaptation routine which {relocates} the active communication behavior from one location to another is precluded by consistency.
%: adaptation is blocked as long as the intended location contains active sessions.
%In some cases, the protection for locations enforced by consistency which may be problematic. %, forcing a relocation to occur only upon session completion may even defeat its purpose. 
Rather than forbidding adaptation steps over locations with active sessions, it would be preferable to 
enable only those steps which preserve such sessions. This suggests the need for ways of tracking the state of the sessions (protocols) running in any given location; this would allow to assess at runtime whether potential adaptation routines preserve such state or not. 
\end{enumerate}

\noindent To address the two needs above, we propose to appeal to constructs included in the \emph{eventful} session types framework developed by Kouzapas et al.~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}. In fact, 
such a framework allows for non-blocking detection of event/message arrivals (as required by (1) above), 
and defines the dynamic inspection of session types (as required by (2) above). A first main contribution of this paper is the enhancement of 
the approach in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}
%our approach to runtime adaptation %of session-typed processes 
with these two event-based mechanisms.
%integrating these elements of the eventful session framework into our own . We highlight key aspects of this integration:
Key novelties include:
\begin{enumerate}[i.]
\item We treat internal and external adaptation requests as \emph{messages}. Each location is associated to a \emph{queue} of adaptation requests. The \emph{message detector} mechanisms of \cite{Kouzapas12} can then be used to specify adaptation managers which are triggered when a request arrives. Location queues are independent from the session behaviors they enclose; hence, they could serve as an interface between the system and its environment. 
%Also, as message detectors can check for certain messages, one can define adaptation managers for specific kinds of requests.

\item We enhance update processes with the ability of dynamically inspecting the session types in a given location.
This is useful to assess the suitability of adaptation routines at runtime. This enhancement relies on ($a$) a session queue containing the type associated to each running session; and ($b$) a generalized form of the $\mathtt{typecase}$ construct in~\cite{Kouzapas12}, which ``tests'' the state of a series of active sessions prior to enable an adaptation step. Using these enhanced update processes, adaptation actions may safely take place on locations enclosing open sessions. 
\end{enumerate}
\noindent The combination of (i) and (ii) results into a rich framework
 for specifying session communication with  runtime adaptation mechanisms (see~\S\,\ref{s:evadap}).
An associated type system, developed in~\S\,\ref{s:types}, ensures 
 communication safety and consistency for well-typed session processes.
To the best of our knowledge, eventful session constructs have not been used for specifying runtime adaptation concerns; the framework we present here appears to be an  application of the event-based approach not previously identified.

Having introduced an eventful framework for runtime adaptation of session typed processes, several natural questions arise.
For instance, given that adaptation requests are handled at the level of locations, how should be processes organized so to achieve coherent adaptation strategies? Also, would it be possible to structure the event- and adaptation-related elements of the framework in~\S\,\ref{s:evadap} in such a way that the separation between communication and adaptation concerns is made explicit? 
%
To address these issues, our second main contribution is a \emph{compartmentalized} model for communication-centric applications (\S\,\ref{s:arch}).
This model intends to be a basic reference for organizing the elements of the framework in~\S\,\ref{s:evadap} into modular units of communication and runtime adaptation. It enforces the separation between communication behavior, event-related elements (e.g., queues), and adaptation constructs. Our model can be seen as a simple but compelling illustration of (a)~how session process specifications can be expressed and reasoned about at higher levels of abstraction, and (b)~how to define interaction between constructs for communication, state, and adaptation while keeping formal and conceptual separations between the three. We define the formal syntax and semantics for specifications of the compartmentalized model, and argue that the session type system for the ``plain'' processes of~\S\,\ref{s:evadap} scales to compartmentalized processes. 



%\section{Motivation}
%%Before introducing the architecture, which is a conceptual contribution, we should detail 
%We now motivate how the asynchronous framework for eventful sessions of~\cite{Kouzapas12} 
%offers a good basis for specifying runtime adaptation for session-typed processes with running sessions. 
%%This is a simple technical contribution; it is desirable to understand well these technical issues before building a whole architecture upon them.
%In the rest of this section, we assume 
%the syntax, semantics, and typing system of~\cite{Kouzapas12}.
%
%\subsection{Updating Processes With Open Sessions I: Queues}
%What we borrow from that framework in~\cite{Kouzapas12} is actually only a few things: 
%(i)~their use of the current state of a session, recorded in an associated queue; 
%(ii)~their use of subtyping inside the reduction semantics.
%
%We add to the syntax of~\cite{Kouzapas12} two constructs:
%located processes, denoted $\scomponent{\locf{loc}}{P}$, and update actions, written $\nadapt{\locf{loc}}{Q(\til{z}{:}\til{\ST})}$.
%Located processes are as usual. The update action $\nadapt{\locf{loc}}{Q(\til{z}{:}\til{\ST})}$ acts on location $\locf{loc}$
%and contains an adaptation routine $Q$ (a process, not a context) 
%with open sessions $z_1:\ST_1, \ldots, z_n:\ST_n$. %, which implement sessions $\ST_1, \ldots, \ST_n$, respectively.
%We assume that $\mathsf{fc}(Q) = \til{z}$.
%
%
%In~\cite{Kouzapas12}, a queue associated to session $s$ is written $s[S, \mathsf{i}:\overline{h}, \mathsf{o}:\overline{h'}]$. 
%Here, %as we have ran out of symbols, 
%we write $\que{k}{\ST; M}$, where $\ST$ is the current session type for session $k$, with input and output messages $M$. 
%We now extend the reduction semantics of~\cite{Kouzapas12} so as to allow runtime adaptation.
%\begin{equation}\label{eq:redsem}
%\frac{
%\mathsf{fc}(P) = \til{\kappa} \quad 
%\rho = \subst{\til{\kappa}}{\til{z}} \quad
%\til{\STT} \leq \til{\ST} \qquad 
%\mathcal{S}(\til{\ST}) = \que{\kappa^p_1}{\ST_1; M_1} \para \dots \para \que{\kappa^p_n}{\ST_n; M_n}
%}{
%\scomponent{\locf{loc}}{P} \para
%\mathcal{S}(\til{\ST}) \para
%\nadapt{\locf{loc}}{Q(\til{z}{:}\til{\ST})}
%\pired 
%\scomponent{\locf{loc}}{\rho(Q)} \para \mathcal{S}(\til{\ST})
%}
%\end{equation}
%This is of course a very simple form of adaptation; still, it captures the essence of the update of a process
%with active sessions:
%\begin{enumerate}[1.]
%\item It does not involve the location $l$. Relocation is not admitted, so the location hierarchy is not disrupted. (Relocation is not particularly dangerous, but philosophically we seek updates that are as preserving as possible; in that line, preservation of location hierarchy seems reasonable.)
%\item It may handle the case in which $P$ has more than one active session
%\item It offers a new implementation for the location $l$, which is identical or better than the current one (up to subtyping)
%\item The state of the located process is preserved (or improved, thanks to subtyping)
%\end{enumerate}
%
%A drawback of this form of adaptation is that there is little control on \emph{when} an adaptation routine (update process) is made available.
%Some alternatives include, for instance, placing it within an if-then-else construct or after a given prefix. 
%These alternatives are internal, in the sense that they must be programmed (i.e., specified) in advance; the possibility of 
%external calls to adaptation routines (say, from a neighboring system not specified) is not present.
%In the following, we explore how to use events to govern the actual availability of adaptation routines.
%
%\subsection{Updating Processes With Open Sessions II: Adding Events}
%The drawback suggested before motivates the use of events for handling adaptation requests.
%We will now assume that locations $l$ will have an associated queue in which requests can be accumulated. 
%Then, by using the $\mathtt{arrive}$ predicate introduced in~\cite{Kouzapas12} within if-then-else expressions, we may 
%spawn the adaptation routine. This means that a possible template for adaptation routines for location $l$ could be the following:
%$$
%M = \mu X.\mathsf{if}~\arrive{l, adp}~\mathsf{then}~l\{Q(\til{z}:\til{\STT})\}~\mathsf{else}~X 
%$$
%with the intuitive meaning: if an adaptation event `$adp$' is detected as present in the queue of location $l$, then 
%spawn an update process; otherwise, if such an event is not detected, recurse.
%
%Notice that by appealing to queues, we can handle both internal and external adaptation requests: 
%as elements of the queue of $l$ are simply detected by $M$, independently of their origin, the associated update prefix
%can be released uniformly. One may also define a class of possible messages for that queue, in order to recognize whether requests are internal or external.
%For instance, we may define $\mathtt{arrive}(l\, int-adp)$ and $\mathtt{arrive}(l\, ext-adp)$.
%This refinement of the $\mathtt{arrive}$ predicate is simple to achieve and can add expressiveness.
%
%A drawback of this form of adaptation is the following.
%Notice that there could be interleaved actions between the moment in which the adaptation request is placed in a queue, 
%and the moment in which the update prefix is actually released. 
%In particular, it could occur that an update prefix that is appropriate for $l$ when the request is detected, 
%is no longer appropriate when the update prefix is ready to interact. A simple solution is to add a form of \emph{stopping}
%a location as soon as the adaptation event is detected. Precisely, we could 
%add a new prefix $\mathsf{stop}\, l$ to the language, with the following associated reduction rule
%$$
%l[P] \parallel \mathsf{stop}\, l;Q \pired l[\![P]\!] \parallel Q
%$$
%where $ l[\![P]\!]$ intuitively represents a located process in which $P$ can no longer evolve. 
%(These stopped located processes would only arise at runtime.)
%One would then re-define rule \eqref{eq:redsem} in terms of stopped located processes. 
%Finally, by defining 
%$$
%M' = \mu X.\mathsf{if}~\mathtt{arrive}(l\, adp)~\mathsf{then}~\mathsf{stop}\, l; l\{Q(\til{z}:\til{\STT})\}~\mathsf{else}~X 
%$$
%we could reduce the possibilities that the located process at $l$ modifies its sessions prior to 
%the release of the adaptation routine. %, thus ruling out potential adaptation routines.
%
%\subsection{Updating Processes With Open Sessions II: Adding Typecase}
%Although the use of events brings uniformity to adaptation, by itself it is not very precise.
%In fact, even with the addition of the $\mathsf{stop}$ prefix we could find discrepancies between 
%the issue of an adaptation request and the associated response offered by processes such as $M$ and $M'$.
%What we require is a mechanism which handles adaptation with the actual current state of all the sessions enclosed by a location.
%
%In~\cite{Kouzapas12}, the authors introduce a \emph{session typecase} operator, written 
%$$\mathsf{typecase}\,k\,\mathsf{of}\,\{(x_i : S_i) : P_i\}$$
%Informally, this operator  
%attempts to match the current (i.e. run-time) session type of channel $k$ 
%against the specified session types $S_i$, proceeding to the $P_i$ for the first $S_i$ that matches.
%We propose to modify this operator in two ways. First, 
%we generalize it so as to consider more than one session.
%The typecase would then consider the combination of the state of two or more sessions.
%Second, we embed it within update processes. The result is the following \emph{typeful update prefix}:
%$$l\big\{\mathsf{case}\,k_1,\ldots,k_n\,\mathsf{of}\,\{(x_{1i} : \ST_{1i}; \cdots; x_{ni} : \ST_{ni}) : Q_i\} \big\}$$
%which we abbreviate as 
%$$l\big\{\mathsf{case}\,\overline{k}\,\mathsf{of}\,\{(\overline{x_{i} : \ST_{i}}) : Q_i\} \big\}$$
%We may then re-define  rule \eqref{eq:redsem} as follows (roughly, some details to be checked):
%\begin{equation}\label{eq:redsem2}
%\frac{
%fc(P) = \til{\kappa} \quad 
%\rho = \subst{\til{\kappa}}{\til{z}} \quad
%\til{\STT} \leq \til{\ST} \qquad 
%\mathcal{S}(\til{\ST}) = \kappa_1\lfloor \ST_1; M_1 \rfloor \parallel \dots \parallel \kappa_n\lfloor \ST_n; M_n \rfloor
%}{
%l[P] \parallel 
%\mathcal{S}(\til{\ST}) \parallel
%%l\{Q(\til{z}:\til{\STT})\}
%l\big\{\mathsf{case}\,\overline{\kappa}\,\mathsf{of}\,\{(\overline{z_{i} : \STT_{i}}) : Q_i\} \big\}
%\pired 
%l[\rho(Q_k)] \parallel \mathcal{S}(\til{\ST})
%}
%\end{equation}
%where $Q_k$ is the adaptation behavior that is associated to a good match for all the $n$ sessions involved.
%Then, by appealing to events, we could define
%$$
%M'' = \mu X.\mathsf{if}~\mathtt{arrive}(l\, adp)~\mathsf{then}~l\big\{\mathsf{case}\,\overline{\kappa}\,\mathsf{of}\,\{(\overline{z_{i} : \STT_{i}}) : Q_i\} \big\}~\mathsf{else}~X 
%$$
%Intuitively, with the typeful update process we could explicitly define how to update a given location $l$, depending 
%on the current state of the protocols running in $l$. This update process can be as detailed as required: it allows to exhaustively specify how different states for the different sessions can lead to different adaptation routines $Q_k$. This brings extended precision to the specifications, also considering possible interleavings, as explained earlier when motivating a stop prefix for locations.
%
%It will be useful to have typeful update processes which are \emph{complete}; that is, 
%adaptation routines in the sense that, using session types, cover all possibilities for all involved sessions. One could also define a default option for typeful updates, to be carried out when none of the specified combinations of sessions actually matches.
%
%% \subsection{Some further issues}
%% Some further issues: 
%% \begin{itemize}
%% \item the typeful update should be defined in terms of variables...how/when the typeful update is instantiated with actual session channels? \\
%% idea: a two-step semantics for update. first, the location is stopped and the case is instantiated. second, the case is evaluated and the location is updated and restarted.
%% \item what if there is a mismatch between the number of open sessions in a given location, and the number of sessions that the update handles?
%% \end{itemize}

\section{The Process Model: Syntax and Semantics}\label{s:evadap}
%ADD POINTERS TO TYPES (duality, subtyping)


\begin{table}[t!]
$$
\begin{array}{lrlr}
u & ::=  &   x, y  \sepr a, b & \text{names}	\\
 k & ::=  &   x, y \sepr \cha^{+}, \cha^{-} & \text{channels}	\\
%d & ::= & a, b  \,\sepr \cha^{+}, \cha^{-} & \text{identifiers} \\
%v & ::= & \mathtt{true}, \mathtt{false} \sepr a, b  \sepr \cha^{+}, \cha^{-} & \text{values} \\
r	&::= &  \mathtt{upd}_I \sepr \mathtt{upd}_E \sepr\mathtt{upg} \sepr \cdots &\text{adaptation messages} \\
e & ::= & v \sepr x, y, z  \sepr \cha^{p} = \cha^{p} \sepr a = a & \text{expressions}  \\
%  & \sepr & \arrive{u}  \sepr \arrive{k} \sepr \arrive{k,h} & \text{arrive predicates (usual)}\\ 
  & \sepr & \arrive{\locf{loc}, r} & \text{arrive predicate} \\ 
P & ::=  &   \nopenr{u}{x:\ST}.P  ~~\sepr~~ \nopena{u}{x:\ST}.P  ~~\sepr~~\close{k}.P& \text{session request / acceptance / closure}	 \\
%	& \sepr &   \nopena{u}{x:\ST}.P  & \text{session acceptance}	\vspace{0.5mm} \\
	& \sepr &  \outC{k}{e}.P ~~~~\sepr~~ \inC{k}{x}.P  & \text{data output /input } \\
  %	&\sepr &    \inC{k}{x}.P  & \text{data input} \vspace{0.5mm} \\
	&\sepr&   \select{k}{n};P ~~\sepr~~  \branch{k}{n_i{:}P_i}_{i \in I} & \text{selection / branching} \\
%    &\sepr&   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} & \text{branching} \vspace{0.5mm}\\
%		&\sepr&   \close{k}.P & \text{close session}	 \vspace{0.5mm}\\
    &\sepr&   \mu \rv{X}.P ~~\sepr~~ \rv{X} & \text{recursion / rec. variable}  \\
%	& \sepr &   \rv{X}& \text{recursion variable}  \vspace{0.5mm}\\
  	& \sepr &   P \para  P  ~~\sepr~~   \mathbf{0}  & \text{parallel composition / inaction } \\	 
	&\sepr&   \restr{\cha}{P} ~\sepr~~ \restr{u}{P}  & \text{channel / name hiding}	\\
		  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional} \\
%	&\sepr&   \restr{a}{P}  & \text{name hiding}	\vspace{0.5mm} \\
%	&\sepr&   \mathbf{0}  & \text{inaction} \vspace{1.5mm} \\
	&\sepr&   \que{\cha}{\ST}  & \text{session queue}  \\ 
		&\sepr&  \scomponent{\locf{loc}}{P}  & \text{located process}  \\
%	&\sepr&  \nadapt{l}{P} & \text{update process}\\
	&\sepr&  \nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}} \quad& \text{typeful update process} \\
	&\sepr&   \outC{\locf{loc}}{r} \sepr \que{\locf{loc}}{\til{r}} & \text{adaptation signal / queue} %\vspace{0.5mm} \\
	%&\sepr&   \que{\locf{loc}}{\til{r}}  & \text{queue for locations} 
%p	&::= &  + \sepr - &\text{channel polarities} \\
%h	&::= &  v \sepr n &\text{messages}  
%    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \mathtt{not}(e) \sepr  \ldots & \text{expressions}
\end{array} 
$$
\caption{Session Processes with Runtime Adaptation: Syntax} \label{tab:syntax}
\vspace{-5mm}
\end{table}


%TO DO: mention abbreviations (branching), notation for labels and locations, and close process, annotations for service requests, location messages.

This section introduces our language of processes with sessions and runtime adaptation.
In a nutshell, the language combines the synchronous $\pi$-calculus 
that we have considered in~\cite{DBLP:conf/sac/GiustoP13} with selected features from the eventful session framework in~\cite{Kouzapas12}. We  also give an operational semantics for processes, and illustrate its use with a simple example. \\

\noindent{\bf Syntax.}
Table~\ref{tab:syntax} reports the syntax of our process language, together with the
relevant base sets: names, (session) channels, identifiers, expressions.
In fact, we use polarized channels $\cha^p$, with $p \in \{+,-\}$.
We write $\til{x}$ to denote a finite sequence $x_1, \ldots, x_k$ of variables (and similarly for other  elements).
Processes include usual constructs for session requests and acceptance, session input/output, and labeled choice. 
Common forms of recursion, parallel composition, conditional expressions, and name/channel restriction
are also included.
For session establishment, we rely on annotations with a \emph{session type} $\ST$ and type \emph{duality} $\cdual$; see~\S\,\ref{s:types}.
We also have a prefix for closing a session, inherited from~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}, and useful to structure specifications. %Also, the process syntax includes 
Binding is as follows: 
%the channel 
variable $x$ is bound in processes 
$\nopenr{u}{x{:}\ST}.P$ and $\nopena{u}{x{:}\ST}.P$; similarly, 
$x$ is bound in $\inC{k}{x}.P$. 
Binding for name and channel restriction is as usual.
Also, process variable $\rv{X}$ is bound in  process $\mu \rv{X}.P$.
Based on these intuitions, given a process $P$, its sets of free/bound channels, names, variables, and process variables---noted 
$\mathsf{fc}(P)$, $\mathsf{fn}(P)$, $\mathsf{fv}(P)$, $\mathsf{fpv}(P)$, $\mathsf{bc}(P)$, $\mathsf{bn}(P)$, $\mathsf{bv}(P)$, and $\mathsf{bpv}(P)$, respectively---are defined as expected. 
In all cases, we rely on expected notions of $\alpha$-conversion (noted $\equiv_\alpha$) and (capture-avoiding) substitution.


Up to here, the language is comparable to standard synchronous $\pi$-calculi with sessions. 
Building upon 
\emph{locations} (ranged over $\locf{loc}, \locf{l_1}, \locf{l_2}, \ldots$) and 
\emph{adaptation messages} (ranged over $r, r', \ldots$), 
novel elements in our language are the following: 
\begin{enumerate}[-]
\item runtime queues for channels, denoted $ \que{\cha}{\ST} $; 
\item located processes, denoted $\scomponent{\locf{loc}}{P}$; 
\item eventful update process, denoted $\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}$; 
%\item runtime queues for channels and locations, denoted $ \que{\cha}{\ST} $ and $ \que{\locf{loc}}{\til{r}} $, respectively; 

\item runtime queues for locations, denoted $ \que{\locf{loc}}{\til{r}} $; 
\item adaptation  signals (messages), denoted $\outC{\locf{loc}}{r}$;
\item arrive predicate for locations, denoted $\arrive{\locf{loc}, r}$.
\end{enumerate}
%while located processes have been central in our previous works~\cite{DBLP:conf/sac/GiustoP13,BGPZFMOODS}, constructs (b)--(d) above have been first introduced in~\cite{Kouzapas12}. As 
%we explain in detail next, here we adapt these constructs to the case of runtime adaptation (an issue not explored in~\cite{Kouzapas12}).
We now discuss each of these elements.
As in~\cite{DBLP:conf/sac/GiustoP13,BGPZFMOODS}, given a process $P$ and a location $\locf{loc}$, 
process $\scomponent{\locf{loc}}{P}$ denotes a \emph{located process}.
Locations are transparent: inside \locf{loc}, process $P$ can freely evolve, possibly interacting with its environment. 
They can be nested, which is particularly convenient when structuring processes for adaptability purposes.


\emph{Eventful update processes} rely on the current state of the session protocols running within a given location in order to determine an appropriate adaptation routine. For the sake of clarity, we illustrate first the particular case of \emph{diadic} eventful update processes (i.e., useful to adapt locations with at most two active sessions); then, we discuss the general $n$-adic case. 
A diadic eventful update process is written as follows:
\begin{equation}\label{eq:dya}
\nadaptbig{\locf{loc}}{\mycase{x_1, x_2}{{x_{1}^{}{:}\ST_{1}^{i} \,;\,  x_{2}^{}{:}\ST_{2}^{i}}}{Q_i}{i \in {I}}}
\end{equation}
%Process~\eqref{eq:dya} 
and 
represents an adaptation routine for  sessions %$\cha_1^p, \cha_2^q$ located  at 
enclosed by $\locf{loc}$. 
As formalized by the operational semantics (see below),
this process works  as a case operator on the session protocols currently associated to any channels $\cha_1^p, \cha_2^q$ in \locf{loc}:
if such protocols ``match'' with one of the $\ST^j_1, \ST^j_2$ in the update process, then 
the current behavior at \locf{loc} will be replaced with process $Q_j$.
Otherwise, if no such match is possible, then the behavior at \locf{loc} is left unchanged and the update process at \locf{loc} is consumed. 
Notice that a diadic update process  will be able to update \emph{at most} two sessions established at \locf{loc}. 
This way, e.g., an update process such as~\eqref{eq:dya} could be defined to match only one session (say $\cha_1^p$). 
%This way, for instance, if the current behavior at \locf{loc} involves exactly one running session, and the update process offers an alternative $Q_j$ which requires only a single matching option, then runtime adaptation will be possible.
The general case for eventful update processes (given in (b) above) %is  in Table~\ref{tab:syntax}. It 
generalizes \eqref{eq:dya} by 
handling runtime adaptation for locations with at most $n$ running sessions.
%\begin{equation}
%\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}
%\end{equation}
Note that each option $i \in I$ may refer to a subset of the variables declared as $\til{x}$.

Eventful update processes represent both a generalization and a specialization of the $\mathtt{typecase}$  in~\cite{Kouzapas12}: they are a generalization, for $\mathtt{typecase}$ defines a case-like choice based only on a single session; they are a specialization, for we use dynamic session type inspection only for runtime adaptation purposes. In fact, while in~\cite{Kouzapas12} 
$\mathtt{typecase}$ is part of the syntax of processes, here we limit its use to the case of update processes. This choice enables us to focus on  the key aspects of event-based concurrency that are key to runtime adaptation. Also, it allows us 
%the limited use of our generalized form of $\mathtt{typecase}$ is also useful 
to retain a standard session type syntax; see~\S\,\ref{s:types}. %simplify some parts of our technical development.


Eventful update processes go hand-in-hand with \emph{session queues}, 
which keep the current protocol state  at a given channel. 
Hence, there is a session queue $\que{\cha^p}{\ST}$ for each open session $\cha^p$. 
Session queues are used in~\cite{Kouzapas12} as the medium supporting asynchronous communication. Here we use them only to maintain a type representing the current protocol state. Again, this choice is aligned with our goal of identifying the core elements from the eventful session framework that are central in enhancing runtime adaptation.\looseness=-1
%DA TOGLIERE: Extensions of our framework to the asynchronous case are discussed in Remark X.

\emph{Location queues}, not present in~\cite{Kouzapas12}, 
are associated to locations; they handle adaptation requests, represented by messages $\til{r}$.
%they are denoted $\que{\locf{loc}}{\til{r}}$.
Location queues enable us to give a unified treatment to internal and external adaptation requests, denoted $\mathtt{upd}_I$ and $ \mathtt{upd}_E$, respectively. 
Given $\que{\locf{loc}}{\til{r}}$, it is worth observing that messages $\til{r}$ are not related to communication as abstracted by session types. This directly represents the fact that handling adaptation requests and disciplining session exchanges are orthogonal issues. 
An \emph{adaptation signal} $\outC{\locf{loc}}{r}$ enqueues request $r$ into the location queue of $\locf{loc}$.
To this end, as detailed below, the operational semantics defines synchronizations between adaptation signals and location queues.
%
Clearly, runtime adaptation and communication are not unrelated phenomena: they may be related by coupling eventful update processes and the \emph{arrive predicate on locations}. %, denoted \arrive{\locf{loc}, r}. %, which we now explain.
Inspired by the $\mathtt{arrive}$ predicate in~\cite{Kouzapas12}, this predicate detects if an adaptation message $r$ 
%(which may represent a request for adaptation or upgrade) 
has been placed in the queue of  \locf{loc}. 
The arrive predicate %\arrive{\locf{loc}, r} 
is therefore key in realizing our overall vision of event-based runtime adaptation. % that we put forward in this paper. 
%An adaptation request $r$ can be issued by a part of the specified system (an internal request) or by the environment interacting with the system (an external request). In either case, the request is formally issued by adding message $r$ to the queue associated to  location \locf{loc}, which encloses the behavior that should be adapted/modified. 
%Given the coupling between the arrive predicate and update processes, 
%the latter should not occur freely in the process structure, but guarded within conditional constructs that enable adaptation depending on the arrival of some adaptation request. 
%Hence, upon arrival of an adaptation request, such conditional constructs will release the previously guarded update processes, and adaptation may   take place, depending on both the state of the protocols in the given location and the matching options specified by the update process. 
%We formalize these  ideas through the compartmentalized model of \S\,\ref{s:arch}.

Summing up, our process language enables us to formally address several concerns related to runtime adaptation: using adaptation signals and location queues it formally explains 
%\emph{who} may specify/trigger an adaptation event; by using queues  it also decrees 
\emph{how} an adaptation request is issued; by exploiting the arrive predicate we may also specify \emph{when} adaptation will be handled/triggered; using eventful update processes (and session queues) we may precisely specify \emph{what} is the goal of an adaptation event. 



%, noted $\sub{\widetilde{c}}{\widetilde{x}}$ (for data), $\sub{\kappa^p}{{x}}$ (for channels), and $\sub{P}{\mathsf{X}}$ (for processes).


\begin{table}[t!]
\[
\begin{array}{lc}
 \rulename{r:Open} & 
\locc{\nopena{u}{x:\ST}.P} \para  \locd{\nopenr{u}{y:\STT}.Q} \pired \hfill  \\
& \hfill 
\restr{\cha}{\big({\locc{P\sub{\cha^{p}}{x} \para \que{\cha^p}{\ST}}  \para  \locd{Q\sub{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT} }\big) } \quad (\ST \cdual \STT) \vspace{1.5mm} \\

\rulename{r:Com} &
\locc{\outCn{\overline{\cha}^{\,p}}{v}.P \para \que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\STT}}} 
\pired \hfill \\
&\hfill
\locc{P \para \que{\cha^p}{\ST}} \para  \locd{Q\sub{{v}\,}{{x}} \para \que{\cha^{\overline{p}}}{\STT} } \quad (\ST \cdual \STT) %\quad ({e} \downarrow {c}) 
\vspace{1.5mm}
\\
%\rulename{r:Sel} &
%C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \} \para \\
%& D\{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST_j} \}_{j \in J}}  \} 
%\pired \\
%& 
%\hfill C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST_j}} \}  \quad (1 \leq j \leq m)  
\rulename{r:Sel} &
\locc{\branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J}\! \para\!  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}}}\! \para \!
\locd{\select{\cha^{\,\overline{p}}}{n_i};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\STT_j \}_{j \in J}} } \\
& \hfill \pired   C\{P_i \para \que{\cha^p}{\ST_i} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\STT_i} \}  \quad (\ST_i \cdual \STT_i,\, i \in J)  
\vspace{1.5mm}
\\
\rulename{r:Clo} &
\locc{\close{\cha^{\,p}}.P \para \que{\cha^p}{\varepsilon} } \para  \locd{\close{\cha^{\,\overline{p}}}.Q \para \que{\cha^{\overline{p}}}{\varepsilon}} \pired %\\
%& \hfill 
\locc{P} \para  \locd{Q} \vspace{ 2mm}
\\
\rulename{r:Eva} & \text{if }e \pired e' \text{ then } \evc{E}[e] \pired \evc{E}[e']
\vspace{1.5mm}\\
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{1.5mm}
\\
%\rulename{r:Con} &  \text{if }P \pired P' \text{ then } \locc{P} \pired \locc{P'}
%\vspace{1.5mm}\\
%  \rulename{r:Loc} &
% \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{1.5mm}
% \\ 
%\rulename{r:ResN} & \text{if }P \pired P' \text{ then } (\nu a)P \pired (\nu a)P'
%\vspace{1.5mm}\\
\rulename{r:ResC} &\text{if }P \pired P' \text{ then } (\nu \cha)P \pired (\nu \cha)P'
\vspace{1.5mm}\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{1.5mm}
\\
 \rulename{r:Rec} &
\recu\,\rv X. P \pired P\subst{\recu\,\rv X. P }{\rv X}
\vspace{1.5mm}\\
\rulename{r:IfTr} &
\ifte{\mathtt{true}}{P}{Q} \pired P    \vspace{1.5mm}
\\
% \rulename{r:IfFa} &
%\ifte{\mathtt{false}}{P}{Q} \pired Q   \vspace{1.5mm}\\
\rulename{r:UReq} &  \locc{\que{\locf{loc}}{\til{r}_1}} \para \locd{\outC{\locf{loc}}{r}} \pired 
\locc{\que{\locf{loc}}{\til{r}_1 \cdot r}} \para \locd{\mathbf{0}}
\vspace{1.5mm}\\
\rulename{r:Arr} & \locc{\evc{E}[\arrive{\locf{loc},r}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{b}]}
\para \locd{\que{\locf{loc}}{\til{r}}}  \  ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
\vspace{3mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{r:Upd} & 
\displaystyle\frac{
\begin{array}{rcl} 
\mathsf{fc}(P) = \til{\cha} = \cha_1^p, \ldots, \cha^p_n 
& &
R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} \\
 (V = P \land R' = R) & \bigvee  &
\exists \til{x}_0 \subseteq \til{x}, \rho .\big(
|\til{k}| = |\til{x}_0| \land \til{x}_0 = \{x_1, \ldots, x_g\} ~\land ~
\\ 
& & \qquad \rho = \subst{\til{\cha}\,}{\,\til{x}_0} ~\land~ I' = \{u \in I \,|\, \mathsf{fc}(Q_u) = \til{x}_0\}~\land\\
& & \qquad \exists l \in I'.(\forall j \in [1..n].\forall s \in [1..g].~~ \STT^{l}_s \csub \ST_j ~\land~ \\
&& \qquad 
\forall r < l.\exists j \in [1..n].\exists s \in [1..g].~~\STT^{r}_s \not\csub \ST_j ~\land~
\\
&&  \qquad V = \rho(Q_l) ~\land~
R' = \que{\cha^p_1}{\STT_{1}^l} \para\! \cdots\! \para \que{\cha^p_n}{\STT^{l}_g} 
)  \big)
\end{array}
}{
\begin{array}{l}
\locc{\scomponent{\locf{loc}}{P \para R}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
\pired \qquad \\
\hfill \locc{\scomponent{\locf{loc}}{V \para R'}} \para \locd{\mathbf{0}}
\end{array}
} 
%\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{r:Upd2} & 
%\displaystyle\frac{
%\begin{array}{c} 
%\mathsf{fc}(P) = \til{\cha} = \cha_1^p, \ldots, \cha^p_n \qquad
%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} \\
% (V = P \land R' = R)  ~~\bigvee~~  \\
%\exists \til{x}_0 \subseteq \til{x}, \rho .\big(
%|\til{k}| = |\til{x}_0| \land \til{x}_0 = \{x_1, \ldots, x_g\}  ~\land~ I' = \{u \in I \,|\, \mathsf{fc}(Q_u) = \til{x}_0\}~\land\\
% \exists l \in I'.(\forall j \in [1..n].\forall s \in [1..g].~~ \STT^{l}_s \leq \ST_j ~\land~  
%\forall r < l.\exists j \in [1..n].\exists s \in [1..g].~~\STT^{r}_s \not\leq \ST_j ~\land~ \\
%  \quad  
%\rho = \subst{\til{\cha}\,}{\,\til{x}_0} ~\land ~ V = \rho(Q_l) ~\land~
%R' = \que{\cha^p_1}{\STT_{1}^l} \para \cdots \para \que{\cha^p_n}{\STT^{l}_g} 
%)  \big)
%\end{array}
%}{
%\begin{array}{l}
%\locc{\scomponent{\locf{loc}}{P} \para R} \para
%\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
%\pired \qquad \\
%\hfill \locc{\scomponent{\locf{loc}}{V} \para R'} \para \locd{\mathbf{0}}
%\end{array}
%} 
\end{array}
%\vspace{-3mm}
\]
\caption{Reduction Semantics for Processes: Selected Rules\label{tab:redsem}}
\vspace{-5mm}
\end{table}
%\vspace{-3mm}

\noindent{\bf Semantics.}
The semantics of our process language is given by a \emph{reduction semantics},
denoted $P \pired P'$, 
the smallest relation on processes generated by rules included those in Table~\ref{tab:redsem}.
It relies on an evaluation relation on expressions, denoted $e \downarrow v$, 
and on a structural congruence, denoted $\equiv$ (see Definition~\ref{d:strcong}). %. (TO BE ADDED)
Moreover, it relies on the following definitions of \emph{evaluation} and \emph{location} contexts:
\begin{eqnarray*}
\evc{E}  ::=  - \sepr \outC{k}{\evc{-}}.P \sepr  \ifte{\evc{-}}{P}{Q} \qquad \quad
C,D  ::=  - \sepr \scomponent{\locf{loc}}{C \para P}
\end{eqnarray*}
Given 
$\locc{\!\!-\!\!}$
 (resp. $\evc{E}[-]$), we write $\locc{P}$ (resp. $\evc{E}[e]$) to denote 
the process (resp. expression) obtained by filling in all occurrences of hole $-$
in $C$ with $P$ (resp. in $\evc{E}$ with $e$). The extension of $\equiv$ to contexts is as expected.

We comment on the rules in Table~\ref{tab:redsem}. The first four rules formalize session behavior within hierarchies of nested locations; they assume the expected notion of duality over a polarity $p$, written $\overline{p}$. In rule~\rulename{r:Open} the synchronization on a channel $u$ with dual session types leads to the establishment of a
fresh session, which in our case entails also the creation of a session queue with the prescribed behavior.
Observe that such queues are created in the same located contexts where session establishment occurs. Hence, all session queues are \emph{local} by construction. 
Rule~\rulename{r:Com} represents session communication of a value: following~\cite{Kouzapas12}, in addition to requiring complementary prefixes, we also require that the type in associated session queues supports an input and output behavior. After the reduction, prefixes in both processes and session types are consumed.  
This is key to properly track the evolution of session protocols. Rule~\rulename{r:Sel} for labeled choice is standard, augmented with session queues. Rule~\rulename{r:Clo} formalizes coordinated session termination. 
%It is worth observing that we require that session queues are \emph{local} to the process. This way, for instance, a process 
%\begin{equation}
%\locc{\outCn{\overline{\cha}^{\,p}}{v}.P} \para \loccp{\que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\overline{\ST}}} \nonumber
%\end{equation}
%is not able to reduce for the queue $ \cha^p$ is not local to the process executing that session.
The following six rules in the table define
standard and/or self-explanatory treatments for, respectively, reduction under evaluation contexts, parallel composition, located context, and restriction; applications of structural congruence; recursion and conditional operators. 

The last three rules in Table~\ref{tab:redsem} define the event-based approach to runtime adaptation. Rule~\rulename{r:UReq} assimilates the issue of an adaptation request to a synchronization between a queue and an adaptation message. The queue and the message may be in different location contexts;  this enables ``remote'' adaptation requests. Rule~\rulename{r:Arr} resolves arrive predicates within evaluation contexts; it queries the current content of the (possibly remote) queue. Rule~\rulename{r:Upd} gives semantics to eventful update process. While at a first sight it may appear complex, the rule actually enforces a simple case operation over the running sessions at location \locf{loc}. The rule attempts to match (via subtyping, noted  $\csub$ in~\S\,\ref{s:types}) the current protocol state at \locf{loc} (embodied by the open sessions $\til{\cha}$ and their associated queues $R$) with the different options offered by the update process. The rule focuses on finding the first positive match; if no such 
match exists then the current behavior at \locf{loc} ($P$, in the rule) is left unchanged, and the update process is consumed.\looseness=-1 





\noindent{\bf Example.}
Consider %the following simple scenario.
%Consider the following processes. We have 
a single-instance service (on name $u$) and a corresponding client; they reside in 
different 
locations, denoted  \locf{ser} and \locf{cli}, respectively. 
The server is associated to a manager $M_\locf{ser}$ which should spawn an adaptation routine %$A_\locf{ser}$ 
in two cases:
\begin{enumerate}[(1)]
\item A known component of the system (the client or the server itself) issues an adaptation request for service $u$.
\item A non specified part of the system (say, its surrounding environment) issues an adaptation request.
\end{enumerate}
%\noindent We will proceed to illustrate the following distinctive aspects of our framework:
%\begin{enumerate}[$-$]
%\item The use of typeful update processes to enforce runtime adaptation that depends on the state of the running sessions.
%\item The use of adaptation requests inside processes to invoke adaptation routines.
%\item How to handle external adaptation requests.
%\end{enumerate}
%\noindent 

\noindent We may formalize the scenario as follows (assuming $\ST \cdual \STT$):
\begin{eqnarray*}
Sys & =  & \scomponentbig{\locf{ser}}{ \nopena{u}{x{:}\ST}.\branchbig{x}{ l_1{:}Q_x \alte l_2{:}\branch{x}{n_1{:}P_x^1 \alte n_2{:}P_x^2}} \para M_\locf{ser}} \para \scomponentbig{\locf{cli}}{ \nopenr{u}{y{:}\STT}.R_y }  \\
%& = & ~\scomponentbig{\locf{cli}}{ \nopenr{u}{y:\ST}.(\outC{\locf{ser}}{\mathtt{upd}_I} \para \select{y}{l_2};\select{y}{n_2};R'_y) } \\
%&   & ~\scomponentbig{\locf{cli}}{ \nopenr{u}{y{:}\overline{\ST}}.R_y } \\
M_\locf{ser} & =  & \que{\locf{ser}}{\epsilon} \para \mu \rv{X}.\ifte{\arrive{\locf{ser}, \mathtt{upd}_I}}{A_\locf{ser}}{\rv{X}}
 \\
& & \qquad  ~~\para \mu \rv{X}.\ifte{\arrive{\locf{ser}, \mathtt{upd}_E}}{B_\locf{ser}}{\rv{X}}
\end{eqnarray*}
where we assume $\ST = \&\{l_1{:}\alpha_1\,,\,   l_2{:}\&\{n_1{:}\alpha_{21} \,,\,  n_2{:}\alpha_{22} \}\}$.
Thus, the service on  $u$ offers two options to the client, distinguished with labels $l_1$ and $l_2$.
If the second option is selected, a further choice becomes available with labels $n_1$ and $n_2$. Notice that 
all of these possibilities entail different behaviors (denoted $Q_x$, $P_x^1$, and $P_x^2$, respectively). 
Observe also that   $M_\locf{ser}$ includes three components: (a)~the queue for adaptation requests (internal or external) for the service
at \locf{ser}; (b)~a process ready to react if an internal adaptation request arrives;
and (c)~a process which reacts to external adaptation requests. 

Suppose now that client and 
service interact on $u$ to establish the session. 
Assume further that the client's body $R_y$ includes, in addition 
to their communication behavior, 
 the issue of an adaptation request 
for the service. 
This is a natural possibility for clients, for they would like to interact with the latest available version of the service:
\begin{equation}
R_y = \outC{\locf{ser}}{\mathtt{upd}_I} \para \select{y}{l_2};\select{y}{n_2};R'_y \nonumber
\end{equation}
Hence, after the synchronization on $u$ we obtain:
\begin{eqnarray*}
Sys & \pired  & \scomponentbig{\locf{ser}}{\branchbig{\cha^+}{ l_1{:}Q_{\cha^+} \alte l_2{:}\branch{\cha^+}{n_1{:}P_{\cha^+}^1 \alte n_2{:}P_{\cha^+}^2}} \para \que{\cha^+}{\ST} \para M_\locf{ser}} \para \\
&   & ~\scomponentbig{\locf{cli}}{\outC{\locf{ser}}{\mathtt{upd}_I} \para \select{\cha^-}{l_2};\select{\cha^{-}}{n_2};R'_{\cha^{-}}  \para  \que{\cha^-}{\STT}} = Sys_1
\end{eqnarray*}
In a setting with distributed resources and services, it is hard to predict  when the adaptation request issued by the client will  actually be served. This leads to the question: when the request is finally handled, what should be the appropriate adaptation routine for endpoint $\cha^+$? That is, what should be the actual structure of process $A_\locf{ser}$? Let us assume the following alternatives:
\begin{enumerate}[(a)]
\item If the first branching has not been  decided yet (the actual session has not yet started), then add an extra service $l_3{:}Q'$.
\item If both labels $l_2$ and $n_1$ have been selected by the client, then offer an new behavior that replaces $P_{\cha^+}^1$.
Proceed similarly if both $l_2$ and $n_2$ have been selected.
\item Otherwise, if  none of the above options apply then  keep the service as it is.
\end{enumerate}
These alternatives critically rely on the possibility of referring to concrete states within the structure of the session. As such, it goes beyond the adaptation routines expressible in our previous works~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}. We now illustrate how an adaptation routine capturing (a)--(c) can be expressed in our framework. Let us define the following process for $A_\locf{ser}$:
\begin{eqnarray*}
A_\locf{ser}  =  \nadaptbig{\locf{ser}}{\mathsf{case}\,x\,\mathsf{of}\{(x{:}\ST):P^* ~\alte~ (x{:}\ST_{21}):P^3_{x}  ~\alte~ (x{:}\ST_{22}):P^4_{x} \, \}} 
\end{eqnarray*}
where 
$P_x^3$ (resp. $P_x^4$) is an alternative implementation for $P_x^1$ (resp. $P_x^2$), and $P^*$ stands for 
the following extended service definition:
\begin{eqnarray*}
\branchbig{x}{ l_1{:}Q_x \alte l_2{:}\branch{x}{n_1{:}P_x^1 ~\alte n_2{:}P_x^2} \alte l_3{:}Q'_x}
\end{eqnarray*}
With this definition for $A_\locf{ser}$, adaptation can be enforced independently of the actual moment in which 
the internal adaptation request is issued and detected by $M_\locf{ser}$.


%Given the coupling between the arrive predicate and update processes, 
%the latter should not occur freely in the process structure, but guarded within conditional constructs that enable adaptation depending on the arrival of some adaptation request. 
%Hence, upon arrival of an adaptation request, such conditional constructs will release the previously guarded update processes, and adaptation may   take place, depending on both the state of the protocols in the given location and the matching options specified by the update process. 


There are several remarkable points in this example.
First, notice the coupling between the arrive predicate and eventful update processes enforced by $M_\locf{ser}$:
the latter occur guarded within a conditional which depends on the arrive predicate at some given location.
In the model of \S\,\ref{s:arch} we formalize this coupling of update processes and arrive predicates via conditionals.
Also, observe that the adaptation routine given by $A_\locf{ser}$
specifies the cases in which a concrete behavior modification is meant to occur at runtime. 
This is enough, for our semantics includes a ``default'' adaptation: 
if none of the specified cases holds, then the current state of the session will be kept in location $\locf{ser}$.
Moreover, it is worth stressing that the update process in $A_\locf{ser}$ corresponds to the simple case in which only one session needs to be taken into account. Eventful update processes can handle an arbitrary (but finite) number of sessions. This could come in handy when considering, for instance, a location with several different clients for the same service. 
Finally, it is interesting to notice that external adaptation requests are treated analogously. 
Location identities (such as \locf{ser} or \locf{cli}) are public; as such, they could be visible to the external environment
for adaptation purposes. We believe that this brings uniformity to specifications, and allows us to consider open systems for adaptation purposes.



\section{Session Types for Eventful Runtime Adaptation}\label{s:types}
This section introduces a session type system for the process language of \S\,\ref{s:evadap}.
Our main result (Theorem~\ref{t:safety}) is that well-typed processes enjoy both \emph{safety} (absence of runtime communication errors)
and \emph{consistency} properties (update actions do not disrupt established sessions).
Our development follows the lines of the system we proposed in~\cite{DBLP:conf/sac/GiustoP13}. 
\begin{definition}[Types]\label{d:types}
The syntax of \emph{basic types} (ranged over by $\capab, \sigma,   \ldots$) 
and \emph{session types} (ranged over by $\ST, \beta, \ldots$)
is as follows:
{%\small
\[
\begin{array}{lclr}
T, S&::=& \capab, \alpha \\
\capab, \sigma & ::= & \mathsf{name} \sepr \mathsf{bool}  ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\capab).\alpha \sepr ?(\capab).\alpha  \sepr !(\beta).\alpha \sepr ?(\beta).\alpha  \quad& \text{send, receive, throw, catch} \vspace{0.5mm}\\ 
		& \sepr &  \&\{n_1{:}\alpha_1 \dots  n_m{:}\ST_m \} \sepr \oplus\{n_1{:}\alpha_1 \dots  n_m{:}\ST_m \}  &  \text{branch, select} \vspace{0.5mm} \\
		& \sepr &  \epsilon \!\!\!\!\!\!& \text{closed session} \vspace{0.5mm} \\
    & \sepr  & t \sepr  \mu t.\alpha & \text{type variable, recursion} 
\end{array}
\]}
\end{definition}

\noindent We recall the intuitive meaning of session types. 
Type $?({\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives booleans or session names (resp. a channel of type $\beta$) 
and continues as $\ST$ afterwards. 
Complementary, type $!({\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends a value (resp. a channel)  and that continues as $\ST$ afterwards.
Type $\&\{n_1:\alpha_1 \dots  n_m:\ST_m \}$ describes a branching behavior:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1 \dots  n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$ and continues as $\ST_j$ afterwards.
Finally, type $\epsilon$ represents a channel with no communication behavior and $\mu t.\alpha$ is used to describe recursive behavior. 

Next we introduce the \emph{subtyping relation} over session types;
following~\cite{DBLP:journals/acta/GayH05}, 
it relies on the coinductive notion of \emph{type simulation} (given by Definition~\ref{def:simul} in the Appendix).



%Observe how  $\subt$ is co-variant for input prefixes and contra-variant for outputs, 
%whereas it is co-variant for branching and contra-variant for choices.


\begin{definition}\label{d:subt}
The coinductive subtyping relation, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{R}$
such that $(T, S) \in \mcc{R}$.
The extension of $\csub$ to typings,  written $\ActS \csub \ActS'$, 
arise as expected.
\end{definition}

Also following~\cite{DBLP:journals/acta/GayH05}, 
the key notion of for session type  \emph{duality} is defined coinductively:


\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{duality relation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\tau \csub \sigma$ and  $\sigma \csub  \tau$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = !(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = \&\{n_1:\ty_1 \dots  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1 \dots  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1 \dots  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1 \dots  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}

% \end{definition}
% 
% We may now define:
% 
% \begin{definition}
The \emph{coinductive duality relation}, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
such that $(T, S) \in \mcc{R}$. 
\end{definition}


Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$.
Based on the syntactic occurrences of session establishment prefixes $\nopenr{a}{x{:}\ST}$, and $\nopena{a}{x{:}\ST}$,
the interface of a process describes the %(possibly persistent) 
services appearing in it.
Thus, intuitively, the interface of a process gives an ``upper bound'' on the services that it  may execute.
We have:


\begin{definition}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements 
$\mathrm{I}$ contains 
assignments from names to session types which are qualified.
More precisely: $\mathrm{I} = \{ \qua\,u{:}\ST ~|~ \qua \in \{\qual, \quau\}\}$, 
%\text{$u$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We write $dom(\INT)$ to denote the set $\{u \mid u:\ST_\qua \in \INT \}$ and  $\#_\INT(a) = h$ to mean that element $a$ occurs $h$ times in $\INT$. 
\end{definition}

Observe how several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces $\INT_1$ and $\INT_2$ is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.
Moreover, we write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
We now define an ordering relation over interfaces, relying on subtyping:

%Next definition, extends the  subtyping relation to interfaces..

\begin{definition}[Interface Ordering] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item $\forall (\qual\,a{:}\ST)$ such that  
 $\#_{\INT_\qual}(\qual\,a{:}\ST) = h$  with $h > 0$,
then  one of the following holds:
\begin{enumerate}[(a)]
\item there exists $h$ distinct elements $(\qual\,a{:}\STT_i) \in \INT'_\qual$ such that 
 $\ST \csub \STT_i$ for $ i \in [1..h]$;
\item there exists $(\quau\,a{:}\STT) \in \INT'_\quau$ such that  $\ST \csub \STT$.
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\STT) \in \INT'_\quau $ and $\ST \csub \STT$, for some $\STT$.
\end{enumerate}


\end{definition}


%\subsection{Environments, Judgments and Typing Rules}
% \begin{table}[t]
% \textsc{Environments}
% $$
% \begin{array}{lclr}
% 		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
% \ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
% \Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment} \vspace{0.5mm} \\
% \Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
% \end{array}
% $$  
% \caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
% \end{table}
% 

\begin{table}[t]
\[
\begin{array}{c}

\inferrule*[right=\rulename{t:LocEnv}]{ }{\typing{\Theta, \locf{loc}:\INT}{\locf{loc}}{\INT}} 
\quad \infer[\rulename{t:Que}]
 {\judgebis{\env{\Gamma}{\Theta}}{\que{\cha}{\ST}}{\type{\cha:\que{}{\ST}}{\emptyset}}}{}
\vspace{1.5mm} \\

\infer[\rulename{t:msg}]
{\typing{\Gamma}{r_1}{\msg}}{} \qquad

\infer[\rulename{t:locQ}]
{\typing{\Gamma}{r_1;\til{r}}{\msg}}
{\typing{\Gamma}{\til{r}}{\msg} & \typing{\Gamma}{r_1}{\msg}}\vspace{1.5mm} \\

\infer[\rulename{t:arrive}]
{\judgebis{\env{\Gamma}{\Theta}}{\arrive{\locf{loc}, r}}{\bool}}
{\typing{\Theta}{\locf{loc}}{\INT} \qquad\typing{\Gamma}{r}{\msg}} \vspace{1.5mm} \\


\inferrule*[right=\rulename{t:Loc} ]
 {
       \typing{\Theta}{\locf{loc}}{\INT} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{\locf{loc}}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\vspace{1.5mm} \\

\infer[\rulename{t:Sig}]
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\locf{loc}}{r}}{\type{\emptyset}{\emptyset}}}
{\typing{\Gamma}{r}{\msg}} \qquad

\infer[\rulename{t:QLoc}]
{\judgebis{\env{\Gamma}{\Theta}}{\que{\locf{loc}}{\til{r}}}{\type{\emptyset}{\emptyset}}}
{ \typing{\Gamma}{\til{r}}{\msg}} \vspace{1.5mm} \\


\infer[\rulename{t:Adapt}]
{\judgebis{\env{\Gamma}{\Theta}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m_j}^{}{:}\STT_{m_j}^{j}}}{Q_j}{j \in J}}}{\type{\emptyset}{\emptyset}}}
{\typing{\Theta}{\locf{loc}}{\INT} & \forall j \in J, \ 
\judgebis{\env{\Gamma}{\Theta}}{Q_i}{\type{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m_j}^{}{:}\STT_{m_j}^{j}}{\INT_j} } \quad \INT_j \intpr \INT}

\vspace{1.5mm} \\
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
\quad
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\vspace{1.5mm} \\
\infer[\rulename{t:Subs} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \intpr \INT'}
\vspace{1.5mm} \\
 
 \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST_1, \cha^-:\que{}{\ST_1}, \cha^+:\ST_2, \cha^+:\que{}{\ST_2} }{ \INT}} & \ST_1 \cdual \ST_2} \vspace{1.5mm} \\
 
 \infer[\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{a}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_a}} \quad  \ a \notin \dom{\INT} }\\
 \text{ where } \INT_a \text{ contains only declarations for } a \ (i.e. \forall b\neq a, b\notin \dom{\INT_a} )
 
\end{array}
 \]
\caption{Well-typed processes: Selected Rules} \label{tab:ts}
\vspace{-8mm}
\end{table}

\noindent We now define the typing environments our type system relies on:
\[
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \STT_\qua \rangle \quad& \text{first-order environment (with $\ST_\qua \cdual \STT_\qua$)} \vspace{0.5mm} \\
\Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
\end{array}
\]  
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$. 
Typing $\ActS$ is commonly used to collect
assignments from channels to session types; as such, it describes
currently active sessions. 
In our discipline, 
in $\ActS$ we also include \emph{bracketed assignments}, denoted $\kappa^p:\que{}{\ST}$,
which represent the type for queues. 
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor k^p:\que{}{\ST} \in \ActS\}$. 
We write $\ActS , k:\ST $  where $k \not\in dom(\ActS)$.
$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
In  the interface, a session type is qualified with 
`$\quau$' if it is associated to a persistent service; otherwise, it is qualified with 
`$\qual$'. 
The higher-order environment $\Theta$ 
collects assignments of process variables and locations to interfaces. 
While the former kind of assignments concerns recursive processes, the latter concerns located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
Given these environments, a \emph{type judgment} is  of form\looseness=-1
\[\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}\] 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.
Some selected rules of the type system are shown in Table~\ref{tab:ts}. The rest of the type systems can be found in Appendix \ref{app:types}.
We comment on some  of the rules in Table~\ref{tab:ts}, other rules are standard and/or self explanatory.
Rule \rulename{t:Adapt} types update processes. Notice that the typing rule that ensures each process $Q_i$ has exactly the same active sessions that those declared in the respective case.   The requirement $\INT_j \intpr \INT$ guarantees that the process behavior does not ``exceed'' the expected behavior within the location.
Rule  \rulename{t:Subs}  takes care of  subtyping both for typings $\ActS$ and interfaces. Finally rule~\rulename{t:CRes} types channel restriction that ensures typing duality among partners of a session and their respective queues.
Typing of queues is given by rule \rulename{t:Que} that simply assigns to queue $\que{\kappa}{\ST}$ type $\kappa:\que{}{\ST}$.
Finally rule \rulename{t:NRes} types hiding of service names, by simply removing their declarations from the interface $\INT$ of the process.\looseness=-1



The type system we have introduced satisfies subject reduction that relies on balanced typings: i.e., $\ActS$ is \emph{balanced} iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $\kappa^p:\que{}{\ST} \in \ActS$)
then also 
$\kappa^{\overline{p}}: \STT \in \ActS$ (resp. $\kappa^{\overline{p}}: \que{}{\STT} \in \ActS$), with $\ST \cdual \STT$.
The proof proceeds by induction on the last rule applied in the reduction; it adapts the one given in \cite{DBLP:conf/sac/GiustoP13}.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT'}}$, for some $\INT'$.
\end{theorem}

We now define and state \emph{safety} and \emph{consistency} properties. 
While safety  guarantees  adherence to prescribed session types and absence of runtime errors, consistency ensures that sessions are not jeopardized by incautious  update actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.

\begin{definition}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa$, i.e., 
$P$ is one of the following:
\[
\begin{array}{lclcl}
    \inC{\kappa^{\,p}}{\til{x}}.P' & \qquad &  \outCn{\overline{\kappa}^{\,p}}{v}.P' & \qquad &     \close{\kappa^{\,p}}.P'    \\
   \branch{\kappa^{\,p}}{n_i{:}P_i}_{i \in I}  &  \quad&   \select{\kappa^{\,p}}{n}.P'  & \quad& 
\end{array}
\]
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities.
$P$ is an \emph{error} if
$P \equiv (\nu \til{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{definition}


Informally, a process $P$
is called \emph{consistent} 
if whenever  it has a $\kappa$-redex  then  update actions do not destroy such a redex.  Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$. We then define:

\begin{definition}[Safety, Consistency]\label{d:consis}
Let $P$ be a process.
We say $P$ is \emph{safe} if it never reduces into an error. 
We say $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{definition}


We now state our main result; it follows as a  consequence of Theorem~\ref{th:subred}.
 
\begin{theorem}[Typing Ensures Safety and Consistency ]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then $P$ is update consistent and %never reduces into an error.
safe.
\end{theorem}


%\input{types.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{A Compartmentalized Model of  Communicating Systems}\label{s:arch}
\newcommand{\myapp}[4]{#1\big\langle #2 \,;\, #3\,;\, #4\big\rangle }
\newcommand{\stpar}{\diamond}
\newcommand{\appar}{\parallel}

As discussed  in \S\,\ref{s:evadap}, 
the novel mechanisms for runtime adaptation present in our process language operate at the level of locations.
%The introduction of located processes and mechanisms for runtime adaptation defined over locations 
This raises a natural question: how should  process specifications be organized in order to achieve modular treatment of runtime adaptation? Here we propose an adaptation-oriented model for communicating processes.

Intuitively, our model defines \emph{systems} % are deployed 
in a two-level scheme: from a global perspective, a system is the composition of \emph{applications}, denoted $A_1, A_2, \ldots$. 
%local to each application, we have (located) processes %(as introduced above) 
%with their runtime state.
As we will see, some degree of communication between applications will be allowed.
Each application has a unique identifier, denoted $a_1, a_2, \ldots$.
There are  \emph{handler} processes, denoted $\mathcal{H}_1, \mathcal{H}_2,  \ldots $, responsible for adaptation at the 
system (global) level:  a handler may adapt a service definition at some specific application, or it may affect a whole application.
%Also, there is an initialization process $\mathsf{Init}$ which starts the system by appropriately invoking applications.
%Up to this point, we have:
%\begin{eqnarray}
%Sys & = &  A_1 \appar \cdots \appar A_n \appar \mathcal{H}_1 \appar \cdots \appar \mathcal{H}_k  \nonumber 
%\end{eqnarray}
%where `$\appar$' denotes the parallel composition operator at the system level. 
Applications comprise three   elements: 
\emph{behavior}, \emph{state}, and an \emph{adaptation manager}.
While the first 
contains located service definitions and invocations, the second stores session and location queues associated to the behavior of the application, together with a queue for the application. Finally, the manager implements adaptation policies at the application (local) level. This scheme thus realizes the desired separation of concerns.

%Let us define the syntax of our architecture:
%\begin{eqnarray*}
%Sys & = & A_1 \parallel \cdots \parallel A_n \parallel \mathcal{H} \parallel  \mathsf{Init} \\
%A_i& = & id\langle R \,, S\, , \mathcal{M} \rangle \\
%R & ::= & \scomponent{\locf{loc}}{!a(x).P}   \sepr \scomponent{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
%S & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}}
%\end{eqnarray*}
%\subsubsection*{Definition.} 

More formally, the syntax of processes considered in this section  
is a subset of that introduced in Table~\ref{tab:syntax}: 
\begin{eqnarray*}
P , Q & ::=  &   \nopenr{u@a}{x:\ST}.P  \sepr   \nopena{u}{x:\ST}.P  \sepr   \outC{\locf{loc}}{r}   \\
& \sepr &   \outC{k}{e}.P  \sepr   \inC{k}{x}.P
	\sepr   \select{k}{n};P  
   \sepr   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} 
    \sepr   \close{k}.P   \\
   & \sepr &  \mu \rv{X}.P  
	\sepr   \rv{X} 
  	\sepr   \ifte{e}{P}{Q}  
  	\sepr    P \para  P  	 
		\sepr    \restr{\cha}{P}   
	 \sepr   \restr{a}{P}   
	 \sepr   \mathbf{0}   
\end{eqnarray*}
Our set of processes 
is thus comparable to most session $\pi$-calculi, only extended with the adaptation request $\outC{\locf{loc}}{r}$.
Also, we consider a minor variation in the syntax of session requests, with a reference to an application $a$.
%The need for reference will become clear later on. 
%Let us assume the following abbreviations:
We shall write $\ast\ift{cond}{P}$ 
and $\repopen{u}{x{:}\ST}.P$
to stand for $\mu \rv{X}.\ifte{cond}{P}{\rv{X}}$ and $\mu \rv{X}.\nopena{u}{x{:}\ST}.(P \para \rv{X})$, respectively. 
%\begin{eqnarray}
%\ast\ift{cond}{P} & \triangleq & \mu \rv{X}.\ifte{cond}{P}{\rv{X}} \nonumber \\
%\repopen{u}{x{:}\ST}.P & \triangleq & \mu \rv{X}.\nopena{u}{x{:}\ST}.(P \para \rv{X})  \nonumber
%\end{eqnarray}
Also, we write $P^{-}$ to denote the syntax of processes without service definitions $\nopena{u}{x{:}\ST}.P$.
As it will be clear later on, this is useful to isolate service definitions. 

Building upon processes, our model of compartmentalized communicating systems is defined by the syntax in Table~\ref{t:model}.
%Recall that $\locf{loc}, \locf{l}_1, \locf{l}_2, \ldots$ range over locations. 
%We write $G, G_1, G_2, \ldots$ to denote elements at the global (system) level. 
A system $G$ is the parallel composition of a finite set of  
applications $A$ with some handlers $\mathcal{H}$. In essence, a handler is a persistent process which 
spawns an adaptation strategy as soon as an adaptation request arrives to an appropriate queue. 
Notice this is the only part of our model where update processes may occur. 
Handlers may \emph{update} the behavior at some particular location or 
% included within an application. 
%They may also 
\emph{upgrade} a whole application. 
%As mentioned above, applications are a compartment for communicating behaviors, 
%their associated state, and related adaptation policies. % are jointly described. 
%Indeed, the structure of applications enforces a separation between behavior and state, but also  a separation with respect to adaptation policies. 
The behavior of an application consists of located processes: 
as before, locations are transparent; here we rule out their nesting, for simplicity. 
%A design criteria in the specification of $R$ is the 
We distinguish  between located processes representing service definitions 
from the located processes which make use of such definitions.
Our operational semantics will ensure that locations enclosing service definitions do not contain open (active) sessions. 
This should be useful to better structure adaptation strategies, for service definitions may simply appeal to upgrades, without concerns of preservation of active sessions. The state $\mathsf{S}$ of an application collects the queues associated to the behavior contained: we consider queues for sessions and locations (as before) but also a queue for the whole application, written $\que{a}{\til{r}}$. We write $\mathsf{S}_1 \stpar \mathsf{S}_2$ to denote the parallel composition of two state elements (queues)  $\mathsf{S}_1$ and $\mathsf{S}_2$. Finally, managers $\mathcal{M}$ follow the same principles of handlers, but restricted to the setting of an application (cf. their associated adaptation message $\mathtt{upd}_I$). 
%In fact, it is worth noticing that managers may act upon the issue of an internal update request $\mathtt{upd}_I$ for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted $\mathtt{upd}_E$ and $\mathtt{upg}$, respectively).

%Notice that we separate the state of an application (its queues) so that handler $\mathcal{H}$ can restart an application by simply erasing the current state.
Overall, our model 
% architecture defines a compartmentalized division the syntactic elements studied in previous sections.
%With respect to adaptation, our model 
enforces  two different granularities for adaptation: a global one, defined by the handler (which may update locations inside applications but also entire applications), and a local one, defined by the manager of each application (which may only update locations within his application). 
%The following definition identifies a number of such conditions:
%\begin{definition}
%We will say that $G$ is a \emph{well-formed system} if it satisfies the following conditions:
%\begin{enumerate}[(a)]
%\item There is at least one application $A$ and one handler $\mathcal{H}$.
%\item For each application $\myapp{a_i}{R_i}{\mathsf{S}_i}{\mathcal{M}_i}$ in $G$, 
%state $\mathsf{S}_i$ contains exactly one application queue $\que{a_i}{\til{r}}$.
%\item For each location $\locf{l}_j$ in $R_i$, there is exactly one location queue 
%$\que{\locf{l}_j}{\til{r}}$ in $\mathsf{S}_i$ and 
%exactly one associated  manager $\mathcal{M}_j$ is part of $\mathcal{M}_i$.
%\item Every manager $\mathcal{M}_k$, part of $\mathcal{M}_i$, only refers to internal adaptation requests for location $\locf{l}_k$ occurring in $R_i$.
%\end{enumerate}
%\end{definition}

\begin{table}[!t]
\begin{eqnarray*}
G & ::= & A \sepr \mathcal{H} \sepr G_1 \appar G_2 \\
A & :: = & \myapp{a}{R}{\mathsf{S}}{\mathcal{M}} \\
\mathcal{H} & ::= & *\,\ift{\arrive{\locf{loc}@a, \mathtt{upd}_E}}{\nadaptbig{\locf{loc}}{R}} \sepr *\,\ift{\arrive{a, \mathtt{upg}}}{\nadaptbig{a}{G}} \\
R & ::= & \scomponentbig{\locf{loc}}{\repopen{u}{x{:}\ST}.P}   \sepr \scomponentbig{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
\mathsf{S} & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}} \sepr \que{a}{\til{r}}  \sepr \mathsf{S}_1 \stpar \mathsf{S}_2 \\
\mathcal{M} & ::= & *\,\ift{\arrive{\locf{loc}, \mathtt{upd}_I}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}} \\
& \sepr & \mathcal{M}_1 \para \mathcal{M}_2 
\end{eqnarray*}
%\vspace{-3mm}
\caption{A Compartmentalized Model of Communicating Systems: Syntax\label{t:model}}
\vspace{-8mm}
\end{table}


It is possible to define a set of well-formedness conditions for systems. 
For instance, we may like to impose that for each application $A$ there should be at least one handler $\mathcal{H}$.
Due to space limitations, we do not present such a definition. Instead, we informally motivate a reduction semantics for
systems.  By giving some interesting rules, we illustrate how such a semantics builds upon that for  ``plain'' processes (cf. \S\,\ref{s:evadap}) but propagating the structural divisions introduced above. 

The following rule  enables remote session establishment.
Since we would like to impose a certain degree of isolation between applications, this will be the only rule admitted at the application level (in what follows, we assume $\ST \cdual \STT$):
\begin{equation} \nonumber
\begin{array}{c}
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x{:}\ST}.P}}{\mathsf{S}_1}{\mathcal{M}_1} \appar  
\myapp{a_2}{\scomponentbig{\locf{l}_2}{\,\nopenr{u@a_1}{y{:}\STT}.Q}}{\mathsf{S}_2}{\mathcal{M}_2} 
  \pired  \\% \vspace{-0.5mm}\\
 \myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x:\ST}.P}}{\mathsf{S}_1}{\mathcal{M}_1} \appar \\
 \myapp{a_2}{\scomponentbig{\locf{l}_2}{\restr{\cha}{( P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y})}}}{
\mathsf{S}_2 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\STT}
}{\mathcal{M}_2} 
\end{array}
\end{equation}
Session establishment within applications is of course allowed:
\begin{equation} \nonumber
\begin{array}{c}
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\nopena{u}{x:\ST}.P} \para \scomponentbig{\locf{l}_2}{\nopenr{u}{y:\STT}.Q}}{\mathsf{S}_1}{\mathcal{M}_1} 
 \pired   \\
 %\hfill 
 \myapp{a_1}{\scomponentbig{\locf{l}_1}{\mathbf{0}} \para \scomponentbig{\locf{l}_2}{ \restr{\cha}{( P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y})}}}{
\mathsf{S}_1 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{{\STT}}
}{\mathcal{M}_1} 
\end{array}
\end{equation}
Notice how the service body ``moves'' from $\locf{l}_1$ to $\locf{l}_2$.
The reduction rule for session communication rule would then be defined as 
\begin{equation} \nonumber
\begin{array}{c}
 \myapp{a}{\scomponentbig{\locf{l}_1}{\outCn{\overline{\cha}^{\,p}}{v}.P \para \inC{\cha^{\,\overline{p}}}{{x}}.Q }}{
\mathsf{S} \stpar 
\que{\cha^p}{!(T).\ST} \stpar
\que{\cha^{\overline{p}}}{?(T).{\STT}} 
}{\mathcal{M}}  
 \pired \\
  \myapp{a}{\scomponentbig{\locf{l}_1}{P \para Q\subst{v}{x} }}{
\mathsf{S} \stpar 
\que{\cha^p}{\ST} \stpar \que{\cha^{\overline{p}}}{{\STT}} 
}{\mathcal{M}} 
\end{array}
\end{equation}
Rules for labeled choice and session closure are as expected.
The treatment of conditionals and arrival predicates also follows the lines of the semantics of \S\,\ref{s:evadap}.
Let us consider rules for runtime adaptation.
The following rules define the two possibilities of adaptation at the global level:
\begin{eqnarray}
\myapp{a}{R}{\mathsf{S}  }{\mathcal{M}} \appar \nadaptbig{a}{ \myapp{a}{R'}{\mathsf{S}'  }{\mathcal{M}'}} \pired \myapp{a}{R'}{\mathsf{S}'}{\mathcal{M}'}  \label{eq:mod1}
 \vspace{1.5mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\myapp{a}{\scomponentbig{\locf{loc}}{P} \para R }{
\mathsf{S}  
}{\mathcal{M}} \appar \nadaptbig{\locf{loc}}{Q} \pired
\myapp{a}{\scomponentbig{\locf{loc}}{Q} \para R }{\mathsf{S}  }{\mathcal{M}} \label{eq:mod2}
 \end{eqnarray}
Rule \eqref{eq:mod1} defines an upgrade adaptation at the application level, with the possibility of 
modifying all three components of the application. In contrast, rule \eqref{eq:mod2} defines the update
of a location inside a particular application. As such, it may come in handy to define, e.g., 
the upgrade of a specific service definition. 
Adaptation decreed by a local manager is handled by the following rule, seemingly similar to~\eqref{eq:mod2}:
\begin{eqnarray*}
\myapp{a}{\scomponentbig{\locf{loc}}{P} \para R }{
\mathsf{S}  
}{\mathcal{M} \para \nadaptbig{\locf{loc}}{Q}}   \pired
\myapp{a}{\scomponentbig{\locf{loc}}{Q} \para R }{\mathsf{S}  }{\mathcal{M}} 
 \end{eqnarray*}
As it can be seen, the differences between the reduction semantics for the ``plain'' processes 
of \S\,\ref{s:evadap} and that for systems are mostly conceptual, rather than technical. 
That is, the higher level of abstraction that is enabled by system descriptions does not result in additional technicalities.
We are therefore confident that the typing system of \S\,\ref{s:types} can be easily extended to systems,
including  guarantees of safety and consistency by typing.






\section{Related Work and Concluding Remarks}
In this paper we have introduced an event-based approach to runtime adaptation of session typed processes. The framework is complemented with a compartmentalized model for organizing processes, their state, and their managers/handlers in a proper structure. \\

\noindent{\bf Related Work.}
%The closest related work is the PhD thesis of Kouzapas~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}, which introduces event-bases processes for asynchronous communication together with a complete framework to test arrival of messages and test types of queues. As mentioned throughout the paper we have been inspired by this machinery but we have considerably changed the domain and scope of application. 
% 
As discussed along the paper, the most related works are by Kouzapas et al.~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}. The first papers on eventful sessions, including theory and implementation aspects, are \cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11}; their associated journal paper is~\cite{KouzapasJ13}. Along the paper we  often refer 1to Kouzapas's PhD thesis~\cite{Kouzapas12}, for it provides a recent unified presentation of the framework. Case studies in~\cite{Kouzapas12} include basic event selectors (a building block in event-driven systems) and transformations between multithreading and event-driven programs; as mentioned above, runtime adaptation of session communication seems to be a novel contribution of this paper. Besides the eventful process constructs, the work in~\cite{Kouzapas12} introduces session set types, which are used to type the $\mathtt{typecase}$ construct. In our case, as our generalized typecase is embedded inside update processes, a standard session type syntax suffices. We refer to our previous works~\cite{BGPZFMOODS,DBLP:conf/sac/GiustoP13} for detailed comparisons with related works on runtime adaptation and (binary, multiparty) session types.\\

\noindent{\bf Concluding Remarks.} 
This paper aimed at identifying the strictly necessary eventful constructs useful to enhance 
%The purpose of this paper is to introduce minimal constructs and highlight strategies to handle 
mechanisms runtime adaptation.  
As such, the present proposal admits several interesting extensions; two of them are 
%, thus, believe that by slightly modifying the present proposal  we can adapt our framework to i) describe 
(i)~\emph{asynchronous} session communications and (ii) \emph{higher-order} runtime adaptation.
As for (i), the framework in~\cite{Kouzapas12} already defines the machinery required for such an extension, which could be incorporated in the framework given here.
Concerning~(ii), we believe that the location queues we have introduced here can be extended in such a way that 
in addition to an adaptation signal, they also receive from the environment a process defining an adaptation routine.
%In the first case, the framework proposed by Kouzapas et al. can be adopted here by simply enriching the information on channel  queues.  The second enhancement can be obtained for instance by allowing location queues to receive together with the adaptation signal an update routine to be executed on the locality. 
Similarly, systems of the compartmentalized model % approach can be followed for architectures where states and managers 
can be refined so as to handle also faults and communication problems. This can be achieved by memorizing not only the current state but also some previous history, thus  allowing  a session to rollback to a ``safe'' past state.

%SEE JOURNAL FOR DISCISSION ON ADAPTATION FOR SESSION TYPES



{\small
\bibliographystyle{abbrv}
\bibliography{referen}
}
%\newpage

\appendix
\section{Supplementary Definitions} \label{app:types}

\begin{definition}[Structural Congruence]\label{d:strcong}
Structural congruence is  
the smallest congruence relation on processes that is generated by the following laws:%\footnote{Cinzia, notice that I have slightly changed the axioms, using $k$ instead of $\kappa$}
$$
\begin{array}{cc}
P \!\para \! Q \!\equiv\! Q \!\para \! P  &
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \\
P \!\para \! \nil \!\equiv\! P  & 
P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
\restr{\kappa}{\nil} \!\equiv\! \nil & \restr{\kappa}{\restr{\kappa'}{P}} \!\equiv\! \restr{\kappa'}{\restr{\kappa}{P}} \\
\restr{\kappa}{P} \!\para \! Q \!\equiv\! \restr{\kappa}{(P \!\para \! Q)} ~~\text{(if $\kappa \not\in \mathsf{fc}(Q)$)} \qquad &
\restr{\kappa}{\component{\locf{loc}}{}{\Delta}{P}} \!\equiv\! \component{\locf{loc}}{}{\Delta}{\restr{\kappa}{P}}  \\
\restr{u}{\nil} \!\equiv\! \nil & \restr{u}{\restr{u'}{P}} \!\equiv\! \restr{u'}{\restr{u}{P}} \\
\restr{u}{P} \!\para \! Q \!\equiv\! \restr{\kappa}{(P \!\para \! Q)} ~~\text{(if $u \not\in \mathsf{fn}(Q)$)} \qquad &
\restr{u}{\component{\locf{loc}}{}{\Delta}{P}} \!\equiv\! \component{\locf{loc}}{}{\Delta}{\restr{u}{P}} 
\end{array}
$$
\end{definition}


The following definition is used by Definition~\ref{d:subt}.


\begin{definition}\label{def:simul}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{type simulation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\capab \bsub \sigma$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = ?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\ty_2, \tyy_2)  \in \mcc{R}$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,!(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\tyy_2, \ty_2)  \in \mcc{R}$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\tau_i, \sigma_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = !(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\sigma_i, \tau_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $m \leq h$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $h \leq m$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}
\end{definition}


\begin{table}[!t]
{\small
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:bool}]
{\typing{\Gamma}{\true, \false}{\bool}}{} 
\qquad
\infer[\rulename{t:name}]
{\typing{\Gamma}{a}{\name}}{} 
\vspace{1.5mm} \\
\infer[\rulename{t:bVar}]
{\typing{\Gamma, x: \bool }{x}{\bool}}{} 
\qquad
\infer[\rulename{t:nVar}]
{\typing{\Gamma, x: \name}{x}{\name}}{} 
\vspace{1.5mm} \\
\infer[\rulename{t:eq}]
{\typing{\Gamma}{d=d}{\bool}}{d=a \vee d=\kappa^p \vee d =x} \qquad 
\infer[\rulename{t:Ser}]
{\typing{\Gamma, u:\langle\ST_\qua, {\STT}_\qua\rangle}{u}{\langle\ST_\qua, {\STT}_\qua\rangle}}{\ST \cdual \STT } 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Accept}]
{\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual  \rangle} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}}}{  \judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\ST}.P}{ \type{\ActS}{\,\INT \addelta u: \ST_\qual}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Request}]
 {\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qua , {\STT}_\qual \rangle} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\STT }{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\STT}.P}{ \type{\ActS}{\,\INT \addelta u: {\STT}_\qual }}} 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}

\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:In}]
{\judgebis{\env{\Gamma, {x}:{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{{x}}.P }{\type{\ActS, k:?({\capab}).\ST}{ \INT}}}
\quad 
\inferrule*[right=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \typing{\Gamma}{e}{\capab}}
{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{{e}}.P}{\type{\ActS, k:!({\capab}).\ST}{ \INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Weakc}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
 
\quad
\inferrule*[right=\rulename{t:Weakn}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad a \notin dom(\INT)}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{a}{P}}{\type{\ActS}{ \INT }}}


\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:If}]
 {
 \typing{\env{\Gamma}{\Theta}}{ e}{\mathsf{bool}} \ 
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \ 
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$
}
\caption{Additional Typing Rules}
\end{table}

\end{document}

The report should contain the following information:
- purpose of the STSM;
- description of the work carried out during the STSM;
- description of the main results obtained;
- future collaboration with host institution (if applicable);
- foreseen publications/articles resulting or to result from the STSM (if applicable);
- confirmation by the host institution of the successful execution of the STSM;
- other comments (if any).


